; COMMAND-LINE: --produce-interpolants -q
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
(set-option :produce-interpolants true)
(set-option :incremental true)
(set-logic QF_LIA)
(declare-fun i3 () Int)
(declare-fun i4 () Int)
(declare-fun i7 () Int)
(declare-fun i8 () Int)
(declare-fun i9 () Int)
(declare-fun i10 () Int)
(declare-fun i11 () Int)
(declare-fun i12 () Int)
(declare-fun i13 () Int)
(declare-fun i14 () Int)
(assert (= i4 2))
(assert (> (- i14) 0))
(assert (= i3 2))
(assert (= i7 0))
(assert (= i9 0))
(assert (= i11 0))
(assert (= i13 0))
(get-interpolant A (or (distinct i4 2) (distinct i12 (+ i11 i10)) (distinct i10 (+ i9 i8)) (distinct i8 (+ i7 1)) (distinct i14 (+ i13 i12)) (distinct i3 2)))
(exit)
